A, B:(IdMsgA).
A || B  interface-compatible(A;B)  Feasible(A)  Feasible(B)  Feasible(A  B) 

latex

Definitions

Prop, t  T, M(i), P & Q, A  B, Feasible(D), A || B, P  Q, x:A. B(x), interface-link(A;B;l;tg), P  Q, P  Q, x. t(x), x(s), false, true, i<j, b, tl(l), ij, if b t else f fi, nth_tl(n;as), hd(l), Y, False, A, AB, l[i], ||as||, A & B, , (x  l), x:A. B(x), (xL.P(x)), interface-compatible(A;B), b, P  Q

Lemmas

msga wf, ma-compat wf, interface-compatible wf, ma-sends-on wf, assert wf, finite-type wf, ldst wf, ma-din wf, lsrc wf, ma-dout wf, ma-feasible wf, IdLnk wf, Id wf, ma-join-feasible, l all nil, and functionality wrt iff, l all cons, decidable wf, l all wf, iff transitivity, decidable assert, decidable equal Id, decidable cand, ma-join wf, finite-set-type-cases, l member wf, select wf, le wf, ma-join-sends-on